Termination Proof Script

• Consider the SCC {12-20}. By taking the AF π with π(a__from) = π(A__FROM) = π(cons) = π(from) = π(mark) = π(MARK) = π(s) = 1 and π(A__FIRST) = 2 together with the lexicographic path order with precedence 0 ≻ nil and a__first ≈ first, the rules in {3-13,17-20} are weakly decreasing and the rules in {1,2,14-16} are strictly decreasing. There is one new SCC.
  • Consider the SCC {13,17-20}. By taking the AF π with π(a__from) = π(A__FROM) = π(cons) = π(from) = π(mark) = π(MARK) = 1 and π(a__first) = π(first) = [2] together with the lexicographic path order with precedence a__first ≻ nil and a__first ≈ first, the rules in {3-11,13,17,18,20} are weakly decreasing and the rules in {1,2,19} are strictly decreasing. There is one new SCC.
    • Consider the SCC {13,17,18,20}. By taking the AF π with π(A__FROM) = π(cons) = π(mark) = π(MARK) = π(s) = 1 and π(a__first) = π(first) = [2] together with the lexicographic path order with precedence a__first ≻ nil, a__first ≈ first and a__from ≈ from, the rules in {4-11,13,20} are weakly decreasing and the rules in {1-3,17,18} are strictly decreasing. There is one new SCC.
      • Consider the SCC {20}. There are no usable rules. By taking the AF π with π(MARK) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.